p-first(L)(x) == list_accum(v,f.case v of inl(z) => v | inr(z) => f(x);inr  ;L) 

latex

Definitions	x.A(x), list_accum(x,a.f(x;a);y;l), case b of inl(x) => s(x) | inr(y) => t(y), f(a), inr x ,
FDL editor aliases	p-first